//
// Created by xux on 2024/9/11.
//

#include "Clause.h"

std::vector<int> Clause::exclude_as_vector(int arg) {
    std::vector<int> res;
    for (int i = 0; i < lit.size(); ++i) {
        auto now = get_arg(i);
        if (now != arg) res.push_back(now);
    }
    return res;
}

int Clause::get_arg(int index) {
    return lit[index]>>1;
}

int Clause::get_sign(int index) {
    return lit[index]&1 ? LAB_IN : LAB_OUT;
}

std::list<int> Clause::collect_arg_as_list() {
    std::list<int> res;
    for(int i=0;i<size();i++){
        res.push_back(get_arg(i));
    }
    return res;
}

void Clause::swap(int index1, int index2) {
    std::swap(lit[index1], lit[index2]);
}

void Clause::update_lbd(std::vector<int> depth) {
    std::unordered_set<int> depth_set;
    for(auto &i:lit){
        depth_set.insert(depth[i>>1]);
    }
    lbd = std::min((int)depth_set.size(), lbd);
}

Clause Clause::ClauseBuilder::build(const std::vector<int>& depth) {
    Clause clause;
    clause.lit = std::move(lit);
    std::unordered_set<int> depth_set;
    for(auto &i:clause.lit){
        depth_set.insert(depth[i>>1]);
    }
    clause.lbd = (int)depth_set.size();
    return clause;
}

void Clause::ClauseBuilder::add(int arg, int label) {
    assert(label != LAB_BLANK);
    lit.push_back(arg<<1|(label==LAB_IN));
}
